IrrelevantLambda.agda:8,15-16
Variable x is declared irrelevant, so it cannot be used here
when checking that the expression x has type A
